Nuprl Lemma : imin_ub
13,42
postcript
pdf
a
,
b
,
c
:
. (
a
imin(
b
;
c
))
{(
a
b
) & (
a
c
)}
latex
Up
int
2
,
int
2
Definitions
True
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
bnot
wf
,
lt
int
wf
,
le
wf
,
assert
wf
,
bool
wf
,
le
int
wf
origin
a, b, c:
. (a 
imin(b;c)) 
{(a b) & (a c)} a, b, c:. (a imin(b;c)) {(a b) & (a c)} Q Q Q
Tx:A. B(x)